Nuprl Lemma : scheme-implies-rule
11,40
postcript
pdf
S
:RealizerScheme{i:l}(),
P
,
Q
:(ES
).
S
|-
es
.
P
(
es
)
(
es
:ES.
P
(
es
)
Q
(
es
))
S
|-
es
.
Q
(
es
)
latex
Definitions
x
:
A
.
B
(
x
)
,
f
(
a
)
,
R
||-
es
.
P
(
es
)
,
{
x
:
A
|
B
(
x
)}
,
,
Namer(
n
;
Id_list
)
,
let
x
,
y
,
z
=
a
in
t
(
x
;
y
;
z
)
,
x
:
A
B
(
x
)
,
RealizerScheme{i:l}()
,
S
|-
es
.
P
(
es
)
,
ES
,
x
(
s
)
,
x
:
A
B
(
x
)
,
P
Q
,
Type
,
,
t
T
,
x
.
A
(
x
)
,
x
.
t
(
x
)
Lemmas
R-implies-rule
,
event
system
wf
origin
S:RealizerScheme{i:l}(), P, Q:(ES
).
(es:ES. P(es) Q(es)) S |-es.Q(es) S:RealizerScheme{i:l}(), P, Q:(ES).
(es:ES. P(es) Q(es)) S |-es.Q(es) x:A. B(x)
B(x)B(x) Q
T
x.A(x)
x. t(x)